$\forall$$A$, $C$:Type, $B$:($A$$\rightarrow$Type), $D$:($C$$\rightarrow$Type), ${\it eq}$:EqDecider($C$), $r$:($A$$\rightarrow$$C$), $f$:$a$:$A$ fp$\rightarrow$ $B$($a$).
\\[0ex]($\forall$$a$:$A$. $D$($r$($a$)) = $B$($a$)) $\Rightarrow$ (rename($r$;$f$) $\in$ $c$:$C$ fp$\rightarrow$ $D$($c$))